Nuprl Lemma : fpf-dom-type
11,40
postcript
pdf
X
,
Y
:Type,
eq
:EqDecider(
Y
),
f
:
x
:
X
fp
Top,
x
:
Y
.
strong-subtype(
X
;
Y
)
(
x
dom(
f
))
(
x
X
)
latex
Definitions
A
c
B
,
P
Q
,
P
&
Q
,
S
T
,
P
Q
,
b
,
x
dom(
f
)
,
strong-subtype(
A
;
B
)
,
a
:
A
fp
B
(
a
)
,
x
.
t
(
x
)
,
Top
,
EqDecider(
T
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
deq
wf
,
top
wf
,
fpf
wf
,
strong-subtype
wf
,
fpf-dom
wf
,
assert
wf
,
assert-deq-member
,
strong-subtype-l
member-type
,
subtype-fpf3
origin
X, Y:Type, eq:EqDecider(Y), f:x:X fp
Top, x:Y.
(
x 
dom(f)) (x X) X, Y:Type, eq:EqDecider(Y), f:x:X fp Top, x:Y.
(x dom(f)) (x X) 
B
Q
T Qb dom(f) B(a)
x. t(x)x:A. B(x) T